structure PropLex=
   struct
    structure UserDeclarations =
      struct
(* this lexer only has to be able to lex propositions, so have deleted  *)
(* the agent-specific stuff. Could have left it. Best? *)
open Tokens
type lexresult= Tokens.token
val linenum = ref 1
fun eof _ = Eos			(* hmm...nomenclature! *)
end (* end of user routines *)
exception LexError (* raised if illegal leaf action tried *)
structure Internal =
	struct

datatype yyfinstate = N of int
type statedata = {fin : yyfinstate list, trans: string}
(* transition & final state table *)
val tab = let
val s0 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s1 =
"\003\003\003\003\003\003\003\003\003\042\044\003\003\003\003\003\
\\003\003\003\003\003\003\003\003\003\003\003\003\003\003\003\003\
\\042\003\003\003\003\003\041\040\039\038\003\003\037\036\035\003\
\\033\033\033\033\033\033\033\033\033\033\003\003\031\029\027\003\
\\003\021\021\021\021\021\026\021\021\021\021\021\021\021\021\021\
\\021\021\021\021\025\021\021\021\021\021\021\019\003\017\003\003\
\\003\008\008\008\008\008\008\008\008\008\008\008\008\012\008\008\
\\008\008\008\008\008\008\008\008\008\008\008\007\006\005\004\003\
\\003"
val s8 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\009\000\009\000\010\000\009\000\000\000\000\000\009\000\000\
\\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\009\
\\000\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\
\\000"
val s10 =
"\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\011\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\010\
\\010"
val s12 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\009\000\009\000\010\000\009\000\000\000\000\000\009\000\000\
\\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\009\
\\000\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\009\009\
\\009\015\009\009\009\009\009\009\009\013\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\
\\000"
val s13 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\009\000\009\000\010\000\009\000\000\000\000\000\009\000\000\
\\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\009\
\\000\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\009\009\009\014\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\
\\000"
val s15 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\009\000\009\000\010\000\009\000\000\000\000\000\009\000\000\
\\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\009\
\\000\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\016\009\009\000\000\000\000\000\
\\000"
val s17 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\018\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s19 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\020\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s21 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\022\000\022\000\023\000\022\000\000\000\000\000\022\000\000\
\\022\022\022\022\022\022\022\022\022\022\000\000\000\000\000\022\
\\000\022\022\022\022\022\022\022\022\022\022\022\022\022\022\022\
\\022\022\022\022\022\022\022\022\022\022\022\000\000\000\022\022\
\\022\022\022\022\022\022\022\022\022\022\022\022\022\022\022\022\
\\022\022\022\022\022\022\022\022\022\022\022\000\000\000\000\000\
\\000"
val s23 =
"\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\024\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\023\
\\023"
val s27 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\028\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s29 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\030\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s31 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\032\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s33 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\034\034\034\034\034\034\034\034\034\034\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
val s40 =
"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\009\009\009\009\009\009\009\009\009\009\009\009\009\009\009\
\\009\009\009\009\009\009\009\009\009\009\009\000\000\000\000\000\
\\000"
val s42 =
"\000\000\000\000\000\000\000\000\000\043\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\043\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
\\000"
in Vector.fromList
[{fin = [], trans = s0},
{fin = [], trans = s1},
{fin = [], trans = s1},
{fin = [(N 81)], trans = s0},
{fin = [(N 28),(N 81)], trans = s0},
{fin = [(N 16),(N 81)], trans = s0},
{fin = [(N 18),(N 81)], trans = s0},
{fin = [(N 14),(N 81)], trans = s0},
{fin = [(N 76),(N 81)], trans = s8},
{fin = [(N 76)], trans = s8},
{fin = [], trans = s10},
{fin = [(N 76)], trans = s0},
{fin = [(N 76),(N 81)], trans = s12},
{fin = [(N 76)], trans = s13},
{fin = [(N 59),(N 76)], trans = s8},
{fin = [(N 76)], trans = s15},
{fin = [(N 55),(N 76)], trans = s8},
{fin = [(N 12),(N 81)], trans = s17},
{fin = [(N 41)], trans = s0},
{fin = [(N 10),(N 81)], trans = s19},
{fin = [(N 38)], trans = s0},
{fin = [(N 67),(N 81)], trans = s21},
{fin = [(N 67)], trans = s21},
{fin = [], trans = s23},
{fin = [(N 67)], trans = s0},
{fin = [(N 24),(N 67),(N 81)], trans = s21},
{fin = [(N 26),(N 67),(N 81)], trans = s21},
{fin = [(N 48),(N 81)], trans = s27},
{fin = [(N 51)], trans = s0},
{fin = [(N 81)], trans = s29},
{fin = [(N 33)], trans = s0},
{fin = [(N 43),(N 81)], trans = s31},
{fin = [(N 46)], trans = s0},
{fin = [(N 79),(N 81)], trans = s33},
{fin = [(N 79)], trans = s33},
{fin = [(N 20),(N 81)], trans = s0},
{fin = [(N 35),(N 81)], trans = s0},
{fin = [(N 22),(N 81)], trans = s0},
{fin = [(N 8),(N 81)], trans = s0},
{fin = [(N 6),(N 81)], trans = s0},
{fin = [(N 81)], trans = s40},
{fin = [(N 30),(N 81)], trans = s0},
{fin = [(N 4),(N 81)], trans = s42},
{fin = [(N 4)], trans = s42},
{fin = [(N 1)], trans = s0}]
end
structure StartStates =
	struct
	datatype yystartstate = STARTSTATE of int

(* start state definitions *)

val INITIAL = STARTSTATE 1;

end
type result = UserDeclarations.lexresult
	exception LexerError (* raised if illegal leaf action tried *)
end

fun makeLexer yyinput = 
let 
	val yyb = ref "\n" 		(* buffer *)
	val yybl = ref 1		(*buffer length *)
	val yybufpos = ref 1		(* location of next character to use *)
	val yygone = ref 1		(* position in file of beginning of buffer *)
	val yydone = ref false		(* eof found yet? *)
	val yybegin = ref 1		(*Current 'start state' for lexer *)

	val YYBEGIN = fn (Internal.StartStates.STARTSTATE x) =>
		 yybegin := x

fun lex () : Internal.result =
let fun continue() = lex() in
  let fun scan (s,AcceptingLeaves : Internal.yyfinstate list list,l,i0) =
	let fun action (i,nil) = raise LexError
	| action (i,nil::l) = action (i-1,l)
	| action (i,(node::acts)::l) =
		case node of
		    Internal.N yyk => 
			(let val yytext = substring(!yyb,i0,i-i0)
			     val yypos = i0+ !yygone
			open UserDeclarations Internal.StartStates
 in (yybufpos := i; case yyk of 

			(* Application actions *)

  1 => (inc linenum; lex())
| 10 => (Lsq)
| 12 => (Rsq)
| 14 => (Lset)
| 16 => (Rset)
| 18 => (VBar)
| 20 => (Point)
| 22 => (Comma)
| 24 => (Truet)
| 26 => (Falset)
| 28 => (Nott)
| 30 => (Andt)
| 33 => (Impt)
| 35 => (Dash)
| 38 => (LLsq)
| 4 => (lex())
| 41 => (RRsq)
| 43 => (Langle)
| 46 => (LLangle)
| 48 => (Rangle)
| 51 => (RRangle)
| 55 => (Maxt)
| 59 => (Mint)
| 6 => (Lbrack)
| 67 => (Vart yytext)
| 76 => (Actt yytext)
| 79 => ((* Allow Timet 07 etc. *)
	     Timet (List.foldl (fn(a,r)=>ord(a)-ord(#"0")+10*r)
					0 (explode yytext)))
| 8 => (Rbrack)
| 81 => (raise Error ("logiclex: unrecognised input "^yytext))
| _ => raise Internal.LexerError

		) end )

	val {fin,trans} = Vector.sub(Internal.tab, s)
	val NewAcceptingLeaves = fin::AcceptingLeaves
	in if l = !yybl then
	     if trans = #trans(Vector.sub(Internal.tab,0))
	       then action(l,NewAcceptingLeaves
) else	    let val newchars= if !yydone then "" else yyinput 1024
	    in if (size newchars)=0
		  then (yydone := true;
		        if (l=i0) then UserDeclarations.eof ()
		                  else action(l,NewAcceptingLeaves))
		  else (if i0=l then yyb := newchars
		     else yyb := substring(!yyb,i0,l-i0)^newchars;
		     yygone := !yygone+i0;
		     yybl := size (!yyb);
		     scan (s,AcceptingLeaves,l-i0,0))
	    end
	  else let val NewChar = Char.ord (List.nth (explode (!yyb), (l)))
		val NewState = if NewChar<128 then Char.ord (List.nth (explode (trans), (NewChar))) else Char.ord (List.nth (explode (trans), (128)))
		in if NewState=0 then action(l,NewAcceptingLeaves)
		else scan(NewState,NewAcceptingLeaves,l+1,i0)
	end
	end
(*
	val start= if substring(!yyb,!yybufpos-1,1)="\n"
then !yybegin+1 else !yybegin
*)
	in scan(!yybegin (* start *),nil,!yybufpos,!yybufpos)
    end
end
  in lex
  end
end
